package com.ecnu.codelearn.software_analysis;

import org.springframework.stereotype.Service;

import java.util.ArrayList;
import java.util.List;

/**
 * @author caopeisheng
 */
@Service
public class ImpToFirstOrderLogicService {
    /**
     * 用于返回的结果
     */
    private List<FirstOrderLogic> resultFirstOrder;

    private String markString = "l";
    private int markIndex = 1;//用于标记的下标

    private static final String INACTIVATED = "inactivated";

    public ImpToFirstOrderLogicService() {
    }

    public ImpToFirstOrderLogicService(int subImpSeq) {
        this.markString = markString + subImpSeq + "_";
    }


    public List<FirstOrderLogic> getResultFirstOrder(ProgramSegment programSegment, String initVarDefStrList) {
        if (programSegment.getProgramSegmentType().equals(ProgramSegmentTypeEnum.CONCURRENT)) {
            return getConcurrentResultFirstOrder(programSegment.getChildProgramSegments(), initVarDefStrList);
        } else {
            return getSerialResultFirstOrder(programSegment, initVarDefStrList, true);
        }
    }

    /**
     * 通过生成的imp语句结构构造一阶逻辑公式(串行imp)
     *
     * @param programSegment    生成的imp语句结构
     * @param initVarDefStrList imp语句的初始变量赋值
     * @return
     */
    public List<FirstOrderLogic> getSerialResultFirstOrder(ProgramSegment programSegment, String initVarDefStrList, boolean addInitialAssignmentFirstOrder) {
        resultFirstOrder = new ArrayList<>();

        String firstStartMark = "m";//imp程序的入口状态
        String endStartMark = "e_m";//imp程序的出口状态

        //添加初始赋值的一阶逻辑公式
        if (addInitialAssignmentFirstOrder) {
            resultFirstOrder.add(new FirstOrderLogic(initVarDefStrList, null, firstStartMark, programSegment.getMark()));
        }

        //添加后续的一阶逻辑公式
        analyzeFirstOrderLogicFormulasFromProgramSegment(programSegment, programSegment.getMark(), endStartMark);

        return resultFirstOrder;
    }

    /**
     * 通过生成的imp语句结构构造一阶逻辑公式(并行imp)
     *
     * @param programSegmentList 生成的imp语句结构集合
     * @param initVarDefStrList  imp语句的初始变量赋值
     * @return
     */
    public List<FirstOrderLogic> getConcurrentResultFirstOrder(List<ProgramSegment> programSegmentList, String initVarDefStrList) {
        resultFirstOrder = new ArrayList<>();
        markIndex = 1;

        String impStartMark = "m";//imp程序的入口状态
        String impEndMark = "e_m";//imp程序的出口状态
        List<String> subImpStartMarks = new ArrayList<>();
        List<String> subImpEndMarks = new ArrayList<>();
        List<String> subImpInactivatedMarks = new ArrayList<>();
        for (int i = 0; i < programSegmentList.size(); i++) {
            subImpStartMarks.add("l" + i + "_1");
            subImpEndMarks.add("e_l" + i + "_1");
            subImpInactivatedMarks.add(INACTIVATED);
        }
        resultFirstOrder.add(new FirstOrderLogic(initVarDefStrList, null, impStartMark, INACTIVATED, null, subImpStartMarks));//添加起始一阶逻辑
        resultFirstOrder.add(new FirstOrderLogic(null, null, INACTIVATED, impEndMark, subImpEndMarks, subImpInactivatedMarks));//添加起始一阶逻辑

        for (int i = 0; i < programSegmentList.size(); i++) {
            ProgramSegment programSegment = programSegmentList.get(i);

            ImpToFirstOrderLogicService thisService = new ImpToFirstOrderLogicService(i);
            List<FirstOrderLogic> subImpFirstOrder = thisService.getSerialResultFirstOrder(programSegment, "", false);

            for (FirstOrderLogic firstOrderLogic : subImpFirstOrder) {
                List<String> subInMarkList = new ArrayList<>();
                List<String> subOutMarkList = new ArrayList<>();
                for (int j = 0; j < programSegmentList.size(); j++) {
                    subInMarkList.add(null);
                    subOutMarkList.add(null);
                }
                subInMarkList.set(i, firstOrderLogic.getInMark());
                subOutMarkList.set(i, firstOrderLogic.getOutMark());

                firstOrderLogic.setSubInMarkList(subInMarkList);
                firstOrderLogic.setSubOutMarkList(subOutMarkList);

                firstOrderLogic.setInMark(INACTIVATED);
                firstOrderLogic.setOutMark(INACTIVATED);
            }

            resultFirstOrder.addAll(subImpFirstOrder);
        }

        return resultFirstOrder;
    }

    /**
     * 通过生成的imp语句结构构造一阶逻辑公式(递归)，构造逻辑参照 https://blog.csdn.net/Campsisgrandiflora/article/details/109447418
     *
     * @param programSegment
     * @param inMark
     * @param outMark
     */
    private void analyzeFirstOrderLogicFormulasFromProgramSegment(ProgramSegment programSegment, String inMark, String outMark) {
        int innerMarkIndex = 2;
        switch (programSegment.getProgramSegmentType()) {
            case LOOP:
                List<ProgramSegment> childProgramSegments = programSegment.getChildProgramSegments();
                ProgramSegment child0 = childProgramSegments.get(0);
                ProgramSegment child1 = childProgramSegments.get(1);
                String compareStr = child0.getSegmentString().trim();
                resultFirstOrder.add(new FirstOrderLogic("(" + compareStr + ")", null, programSegment.getMark(), child1.getMark()));
                resultFirstOrder.add(new FirstOrderLogic("~(" + compareStr + ")", null, programSegment.getMark(), outMark));
                analyzeFirstOrderLogicFormulasFromProgramSegment(child1, child1.getMark(), programSegment.getMark());
                break;
            case BRANCH:
                childProgramSegments = programSegment.getChildProgramSegments();
                child0 = childProgramSegments.get(0);
                child1 = childProgramSegments.get(1);
                compareStr = child0.getSegmentString().trim();

                if (childProgramSegments.size() >= 3) {
                    ProgramSegment child2 = childProgramSegments.get(2);
                    resultFirstOrder.add(new FirstOrderLogic("(" + compareStr + ")", null, programSegment.getMark(), child1.getMark()));
                    resultFirstOrder.add(new FirstOrderLogic("~(" + compareStr + ")", null, programSegment.getMark(), child2.getMark()));
                    analyzeFirstOrderLogicFormulasFromProgramSegment(child1, child1.getMark(), outMark);
                    analyzeFirstOrderLogicFormulasFromProgramSegment(child2, child2.getMark(), outMark);
                } else {
                    resultFirstOrder.add(new FirstOrderLogic("(" + compareStr + ")", null, programSegment.getMark(), child1.getMark()));
                    resultFirstOrder.add(new FirstOrderLogic("~(" + compareStr + ")", null, programSegment.getMark(), outMark));
                    analyzeFirstOrderLogicFormulasFromProgramSegment(child1, child1.getMark(), outMark);
                }
                break;
            case COMPARE:
                resultFirstOrder.add(new FirstOrderLogic(programSegment.getSegmentString().trim(), null, inMark, outMark));
                break;
            case COMPLEX:
                childProgramSegments = programSegment.getChildProgramSegments();
                for (int i = 0; i < childProgramSegments.size(); i++) {
                    if (i == 0) {
                        analyzeFirstOrderLogicFormulasFromProgramSegment(childProgramSegments.get(i), inMark, childProgramSegments.get(i+1).getMark());
                    } else if (i == childProgramSegments.size() - 1) {
                        analyzeFirstOrderLogicFormulasFromProgramSegment(childProgramSegments.get(i), childProgramSegments.get(i).getMark(), outMark);
                    } else {
                        analyzeFirstOrderLogicFormulasFromProgramSegment(childProgramSegments.get(i), childProgramSegments.get(i).getMark(), childProgramSegments.get(i+1).getMark());
                    }
                }
                break;
            case SEQUENCE:
                childProgramSegments = programSegment.getChildProgramSegments();
                for (int i = 0; i < childProgramSegments.size(); i++) {
                    if (i == 0) {
                        analyzeFirstOrderLogicFormulasFromProgramSegment(childProgramSegments.get(i), inMark, childProgramSegments.get(i+1).getMark());
                    } else if (i == childProgramSegments.size() - 1) {
                        analyzeFirstOrderLogicFormulasFromProgramSegment(childProgramSegments.get(i), childProgramSegments.get(i).getMark(), outMark);
                    } else {
                        analyzeFirstOrderLogicFormulasFromProgramSegment(childProgramSegments.get(i), childProgramSegments.get(i).getMark(), childProgramSegments.get(i+1).getMark());
                    }
                }
                break;
            case ASSIGNMENT:
                String[] split = programSegment.getSegmentString().split(":=");
                resultFirstOrder.add(new FirstOrderLogic(programSegment.getSegmentString().trim(), split[0], inMark, outMark));
                break;
            case SKIP:
                resultFirstOrder.add(new FirstOrderLogic("", null, inMark, outMark));
                break;
            case WAIT:
                childProgramSegments = programSegment.getChildProgramSegments();
                FirstOrderLogic subFirstOrderLogic = new FirstOrderLogic("(" + childProgramSegments.get(0).getSegmentString().trim() + ")", null, inMark, inMark);
                subFirstOrderLogic.setTurn(childProgramSegments.get(0).getSegmentString().trim());
                resultFirstOrder.add(subFirstOrderLogic);
                subFirstOrderLogic = new FirstOrderLogic("~(" + childProgramSegments.get(0).getSegmentString().trim() + ")", null, inMark, outMark);
                subFirstOrderLogic.setTurn(childProgramSegments.get(0).getSegmentString().trim());
                resultFirstOrder.add(subFirstOrderLogic);
                break;
            default:
                resultFirstOrder.add(new FirstOrderLogic(programSegment.getSegmentString().trim(), null, inMark, outMark));
                break;
        }
    }

}
